D:Dsys, s:(i:IdM(i).(timed)state), t:, f:({0..t}(i:Idd-world-state(D;i))), d:(IdId).
d-partial-world(D;f;t;s;d)  World 

latex

Definitions

d-world-state(D;i), Dsys, World, d-partial-world(D;f;t';s;d), IdLnk, locl(a), Type, if b then t else f fi , i <z j, t.1, x. t(x), x.A(x), d-decl(D;i), M.Msg, source(l), mlnk(m), {i..j}, Void, i  j < k, P & Q, #$n, a < b, S  T, x:A. B(x), , A  B, A, False, P  Q, f(a), , M.(timed)state, t  T, <a, b>, x:A  B(x), Top, , w-automaton(T;TA;M), M.ds(x), type List, {x:A| B(x)} , s = t, Msg(M), x:AB(x), Action(dec), w-action-dec(TA;M;i), M.dout(l,tg), M.da(a), M(i), , Id, s ~ t, timedState(ds), left + right, Unit, P  Q, P  Q, T, b, b, i z j, True, , t.2, null, inl x , inr x , Knd, rcv(l,tg), kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), [], NullMachine, , x:A.B(x), Msg(da)

Lemmas

it wf, w-null wf, rcv wf, subtype rel self, unit wf, Knd wf, null-action wf, pi2 wf, le int wf, assert wf, bnot wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, le wf, Id wf, nat wf, mlnk wf d, lsrc wf, d-m wf, ma-msg wf, d-decl wf, action wf, ma-tst wf, ma-ds wf, rationals wf, pi1 wf, lt int wf, ifthenelse wf, top wf, bool wf, locl wf, ma-da wf, w-automaton wf, mlnk wf, Msg wf, w-action-dec wf, IdLnk wf, ma-dout wf, dsys wf, int seg wf